enum Value {TRUE,FALSE}


sig Bool in Value{}

sig Stringa{}

sig NomeCitta{}

sig NomeHotel{}

sig Prezzo{}

sig IDPacchetto{}

sig IDImpiegato{}

sig IDUtente{}

sig IDHotel{}

sig Password{}

sig Email{}


// Utente generico dell'applicazione
abstract sig Utente{}

// Utente non registrato a TravelDream
sig UtenteNonRegistrato extends Utente{}


//Utente registrato a TravelDream
sig UtenteRegistrato extends Utente{
	nome: one Stringa,
	cognome: one Stringa,
	email : one Email,
	password : one Password,
	iDutente : one IDUtente
}


//Impiegato di TravelDream
sig Impiegato{
	email : one Email,
	password : one Password,
	iDimpiegato : one IDImpiegato
}

//Mezzo di trasporto 
sig Trasporto{
	andata : one Data,
	ritorno: one Data,
	prezzo : one Prezzo,
	citta1 : one NomeCitta,
	citta2 : one NomeCitta
}

sig Hotel{
	nome : one NomeHotel,
	prezzo : one Prezzo,
	stelle : one Int,
	iDhotel : one IDHotel
}{stelle>=3 && stelle<=6}

sig Escursione{}

sig Data{}

sig Pacchetto{
	hotels : one Hotel,
	mezzoTrasporto : one Trasporto,
	escursioni : some Escursione,
	inizio : one Data,
	fine : one Data,
	inOfferta : one Value,
	iDpacchetto : one IDPacchetto
}



//Non esistono impiegati con lo stesso id
fact{
	no disj i1,i2 : Impiegato | i1.iDimpiegato=i2.iDimpiegato
}

//Non esistono impiegati con la stessa mail
fact{
	no disj i1,i2 : Impiegato | i1.email=i2.email
}

//Non esistono utenti con lo stesso id
fact{
	no disj u1,u2 : UtenteRegistrato | u1.iDutente=u2.iDutente
}


//Non esistono utenti con la stessa mail
fact{
	no disj u1,u2 : UtenteRegistrato | u1.email=u2.email
}


//Non esistono pacchetti con lo stesso id
fact{
	no disj p1,p2 : Pacchetto | p1.iDpacchetto=p2.iDpacchetto
}

//Non esistono mail che siano comuni a un utente e a un impiegato
fact{
	no disj u : UtenteRegistrato, i : Impiegato | u.email=i.email
}

//Non esistono pacchetti che siano in offerta e non in offerta allo stesso tempo
fact{
	no p1 : Pacchetto | p1.inOfferta=TRUE && p1.inOfferta=FALSE
}


//Non esistono trasporti le cui città di arrivo e di partenza siano uguali
fact{
	no t1 : Trasporto | t1.citta1=t1.citta2
}

//Non esistono trasporti in cui le date di andata e ritorno coincidano
fact {
	no t2 : Trasporto | t2.andata=t2.ritorno
}

//Non esistono Hotel con lo stesso id, tuttavia è possibile che abbiano lo stesso nome
fact{
	no disj h1,h2 : Hotel | h1.iDhotel=h2.iDhotel
}

//Non esistono pacchetti le cui date di inizio e fine coincidono
fact{
	no p1 : Pacchetto | p1.inizio=p1.fine
}

//Verifico che le date di partenza dei mezzi di quel pacchetti coincidano effettivamente con 
//le date di andata e ritorno del pacchetto
fact{
	all p1 : Pacchetto | p1.inizio=p1.(mezzoTrasporto.andata) && p1.fine=p1.(mezzoTrasporto.ritorno)
}

	
	

pred show (){
}
 run show

